$\forall$$T$:Type, $f$:($T$$\rightarrow$$T$), $R$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$x$:$T$. $R$($x$,$x$))
\\[0ex]$\Rightarrow$ ($\forall$$x$, $y$, $z$:$T$. ($x$ = $f$($y$)) $\Rightarrow$ ($\neg$($x$ = $y$)) $\Rightarrow$ $y$ is $f$$\ast$($z$) $\Rightarrow$ $R$($y$,$z$) $\Rightarrow$ $R$($x$,$z$))
\\[0ex]$\Rightarrow$ \{$\forall$$x$, $y$:$T$. $x$ is $f$$\ast$($y$) $\Rightarrow$ $R$($x$,$y$)\}